T:Type, t:T, l:IdLnk, ds:x:Id fp Type, f:(State(ds)(T + Top)).
Normal(ds)  R-Feasible(weakSendDoApplyR{a:ut2, tg:ut2}(T; t; l; ds; f)) 

latex

Definitions

Type, t  T, x:A  B(x), Id, x:A. B(x), (x  l), {x:A| B(x)} , x:AB(x), type List, IdLnk, Top, left + right, State(ds), a:A fp B(a), Normal(ds), b, xdom(f). v=f(x)   P(x;v), P  Q, do-apply(f;x), Outcome, x.A(x), s = t, if b then t else f fi , IdDeq, x. t(x), f(x)?z, , Unit, ff, tt, False, True, f(a), case b of inl(x) => s(x) | inr(y) => t(y), Void, x:A.B(x), S  T, suptype(S; T), can-apply(f;x), *1*, weakPrecondSendR2{$a:ut2, $tg:ut2}(T; t; p; l; ds; P; f), R-Feasible(R), weakSendDoApplyR{$a:ut2, $tg:ut2}(T; t; l; ds; f)

Lemmas

weakPrecondSendR2 feasible, unit-fps wf, p-outcome wf, assert wf, can-apply wf, true wf, false wf, btrue wf, bfalse wf, fpf-cap wf, id-deq wf, do-apply wf, normal-ds wf, decl-state wf, top wf, l member wf, Id wf